Double click to show/hide
0: main
14: ERC1155Action.safeTransferFrom
15: FreeCollateralExternal.checkFreeCollateralAndRevert
16: FreeCollateralExternal.checkFreeCollateralAndRevert
17: SettleAssetsExternal.settleAssetsAndReturnPortfolio
18: SettleAssetsExternal.settleAssetsAndReturnPortfolio
19: SettleAssetsExternal.settleAssetsAndFinalize
20: SettleAssetsExternal.settleAssetsAndFinalize
accountContextMustBeReadAndWrittenExactlyOnce-safeTransferFrom(address,address,uint256,uint256,bytes)_main 0_0_0_0_0_0_0_0 0_0_0_0_0_0_0_0 43_0_0_0_0_0_0_0 43_0_0_0_0_0_0_0 0_0_0_0_0_0_0_0->43_0_0_0_0_0_0_0 !B95:bool 44_0_0_0_0_0_0_0 44_0_0_0_0_0_0_0 0_0_0_0_0_0_0_0->44_0_0_0_0_0_0_0 B95:bool 14: ERC1155Action.safeTransferFrom 14: ERC1155Action.safeTransferFrom 43_0_0_0_0_0_0_0->14: ERC1155Action.safeTransferFrom 45_0_0_0_0_0_0_1 45_0_0_0_0_0_0_1 44_0_0_0_0_0_0_0->45_0_0_0_0_0_0_1 61_0_0_0_0_0_0_0 61_0_0_0_0_0_0_0 61_0_0_0_0_0_0_0->45_0_0_0_0_0_0_1 14: ERC1155Action.safeTransferFrom->61_0_0_0_0_0_0_0
Block 0_0_0_0_0_0_0_0: W1 = havoc
W2 = havoc
W3 = havoc
R4 = havoc
W5 = havoc
W6 = havoc
W7 = havoc
W8 = havoc
W9 = havoc
W10 = havoc
W11 = havoc
W12 = havoc
W13 = havoc
W14 = havoc
R15 = havoc
R16 = havoc
W36 = havoc
W37 = havoc
UR38 = havoc
UR39 = havoc
e.msg.sender = havoc
e.msg.value = havoc
args = havoc
R40 = havoc
R41 = havoc
R42 = havoc
R43 = havoc
R44 = havoc
R45 = havoc
R46 = havoc
e.msg.address = havoc
R47 = havoc
e.block.number = havoc
e.block.timestamp = havoc
R48 = havoc
M49 = havoc
R50 = havoc
tacCalldatabuf!0@17 = havoc
R51 = havoc
M52 = havoc
R53 = havoc
R54 = havoc
R55 = havoc
R56 = havoc
tacCalldatabuf!0@19 = havoc
R57 = havoc
M58 = havoc
R59 = havoc
R60 = havoc
R61 = havoc
R62 = havoc
tacCalldatabuf!0@18 = havoc
R63 = havoc
M64 = havoc
R65 = havoc
R66 = havoc
R67 = havoc
R68 = havoc
tacCalldatabuf!0@20 = havoc
R69 = havoc
M70 = havoc
R71 = havoc
R72 = havoc
R73 = havoc
R74 = havoc
tacCalldatabuf!0@15 = havoc
R75 = havoc
M76 = havoc
R77 = havoc
tacCalldatabuf!0@16 = havoc
R78 = havoc
M79 = havoc
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=multi contract setup::
currentContract = 0xce4604a000000000000000000000002a
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=rule parameters setup::
account = havoc
B80 = (0x0<=account)&&(account<=0xffffffffffffffffffffffffffffffffffffffff)
assume B80
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=last storage initialize::
B82 = (0x0<=R4)&&(R4<=0xffffffffffffffffffffffffffffffffffffffff)
assume B82
B84 = (0x0<=R15)&&(R15<=0xffffffffffffffffffffffffffffffffffffffff)
assume B84
B86 = (0x0<=R16)&&(R16<=0xffffffffffffffffffffffffffffffffffffffff)
assume B86
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=assumptions about extcodesize::
B87 = W37[0xce4604a000000000000000000000002a]>0x0
assume B87
B88 = W37[0xce4604a0000000000000000000000028]>0x0
assume B88
B89 = W37[0xce4604a0000000000000000000000029]>0x0
assume B89
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=require forall address a. g_readsToAccountContext(a) == 0::
certoraAssume54731 = forall( QVars(a:bv256 bv256) true&&true&&(UR38:uf(a)==0x0))
assume certoraAssume54731
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=require forall address a1. g_writesToAccountContext(a1) == 0::
certoraAssume54732 = forall( QVars(a1:bv256 bv256) true&&true&&(UR39:uf(a1)==0x0))
assume certoraAssume54732
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=f(e,args)::
TRANSIENT::MetaKey(name=call.trace.push, typ=class analysis.icfg.Inliner$CallStack$PushRecord)=PushRecord(callee=MethodRef(contractAddress=274184521717934524641157099916833587242, sigHash=SigHash(f242432a), attr=COMMON), summary=null, id=16)::
B90 = e.msg.sender<0x10000000000000000000000000000000000000000
assume B90
B91 = e.msg.sender>0x0
B92 = e.msg.sender==0x0
B93 = B91||B92
assume B93
R94 = W36[e.msg.sender]
B95 = R94<e.msg.value
if B95:bool goto 44_0_0_0_0_0_0_0 else goto 43_0_0_0_0_0_0_0

Block 43_0_0_0_0_0_0_0: M100 = args
tacCalldatabuf!4@14 = R40
tacCalldatabuf!36@14 = R41
tacCalldatabuf!68@14 = R42
tacCalldatabuf!100@14 = R43
tacCalldatabuf!132@14 = R44
B102 = 0xa3s<R45
assume B102
R103 = e.msg.sender
B104 = (0x0<=R103)&&(R103<=0xffffffffffffffffffffffffffffffffffffffff)
assume B104
R105 = e.msg.value
B106 = R46==e.msg.address
assume B106
B107 = (0x0<=R46)&&(R46<=0xffffffffffffffffffffffffffffffffffffffff)
assume B107
B108 = (0x0<=R47)&&(R47<=0xffffffffffffffffffffffffffffffffffffffff)
assume B108
R109 = e.block.timestamp
I110 = W36[e.msg.sender] -int e.msg.value
W111 = W36[e.msg.sender] = I110
R112 = W111[0xce4604a000000000000000000000002a]+e.msg.value
B113 = add_noofl:bif(W111[0xce4604a000000000000000000000002a],e.msg.value)
assume B113
W114 = W111[0xce4604a000000000000000000000002a] = R112
::Invoke f args :14::
goto: 0_0_0_0_14_0_19607_0

Block 45_0_0_0_0_0_0_1: assume !B96
assume !B98
TRANSIENT::MetaKey(name=call.trace.pop, typ=class analysis.icfg.Inliner$CallStack$PopRecord)=PopRecord(id=16)::
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::
TRANSIENT::MetaKey(name=cvl.label.start, typ=class java.lang.String)=assert forall address a2. g_readsToAccountContext(a2) == g_writesToAccountContext(a2) && g_readsToAccountContext(a2) <= 1 || g_writesToAccountContext(a2) == 0::
certoraAssert_1 = forall( QVars(a2:bv256 bv256) true&&true&&((true&&true&&true&&true&&(UR324:uf(a2)==UR4194:uf(a2))&&true&&true&&(UR324:uf(a2)<=0x1))||(true&&true&&(UR4194:uf(a2)==0x0))))
assert certoraAssert_1,
TRANSIENT::MetaKey(name=cvl.label.end, typ=class java.lang.Boolean)=true::

Block 44_0_0_0_0_0_0_0: B97 = true
B99 = false
::Parallel assignment for 96, 98, 324, 4194 := 97, 99, 38, 39::
B96 = B97
B98 = B99
UR324 = UR38
UR4194 = UR39

Block 61_0_0_0_0_0_0_0: NOP
::Parallel assignment for 96, 98, 324, 4194 := 1092, 1093, 1366, 4847::
B96 = B1092
B98 = B1093
UR324 = UR1366
UR4194 = UR4847

Block 0_0_0_0_14_0_19607_0: ::14: ERC1155Action.safeTransferFrom::
Previous:
0_0_0_0_0_0_0_0 <-